Nuprl Lemma : alle-at-not-first
11,40
postcript
pdf
es
:ES,
i
:Id,
P
:({
e
:E| loc(
e
) =
i
}
).
e
@
i
.
P
(
e
)
e
@
i
. (
(
first(
e
)))
P
(pred(
e
))
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
pred(
e
)
,
E
,
loc(
e
)
,
Id
,
,
first(
e
)
,
b
,
A
,
x
(
s
)
,
e
@
i
.
P
(
e
)
,
ES
,
x
.
t
(
x
)
,
False
Lemmas
alle-at
wf
,
event
system
wf
,
not
wf
,
assert
wf
,
es-first
wf
,
Id
wf
,
es-loc
wf
,
es-E
wf
,
es-pred
wf
,
es-loc-pred
origin
es:ES, i:Id, P:({e:E| loc(e) = i} 
). e@i. P(e) 
e@i. (
(
first(e))) P(pred(e)) es:ES, i:Id, P:({e:E| loc(e) = i} ). e@i. P(e) e@i. ((first(e))) P(pred(e)) 
T Qx:A. B(x)bAe@i. P(e)
x. t(x)